1. Field of the Invention
This invention relates generally to the field of functional verification of digital designs in systems that use an abstraction for portions of a circuit design to perform the verification proof, and in particular to resolving inconsistencies between the design and abstractions for the design.
2. Background of the Invention
Over the last 30 years, the complexity of integrated circuits has increased greatly. This increase in complexity has exacerbated the difficulty of verifying circuit designs. In a typical integrated circuit design process, which includes many steps, the verification step consumes approximately 70-80% of the total time and resources. Aspects of the circuit design such as time-to-market and profit margin greatly depend on the verification step. As a result, flaws in the design that are not found during the verification step can have significant economic impact by increasing time-to-market and reducing profit margins. To maximize profit, therefore, the techniques used for verification should be as efficient as possible.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among the combinational logic between registers.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical tools to create a HDL-based design.
An increasingly popular technique is to use formal methods to verify the properties of a design completely. Formal methods use mathematical techniques to prove that a design property is either always true or to provide an example condition (called a counterexample) that demonstrates the property is false. Tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include specifications and/or requirements that must be satisfied by the circuit design. Since mathematical properties define the design requirements in pure mathematical terms, this enables analysis of all possible valid input sequences for a given circuit and is akin to an exhaustive simulation. Formal verification methods are therefore exhaustive, when compared for example to simulation methods, and they may provide many benefits, such as reduced validation time, quicker time-to-market, reduced costs, and high reliability.
Performance limits and resource availability inhibit the widespread use of model checking. The resources required to perform verification are typically exponentially related to the number of registers in the circuit model, as well as other characteristics. This is referred to as the “state space explosion” problem. Many conventional model checkers analyze the entire design before proving a particular property, verifying the behavior of the design with all possible input sequences values over time. These model checking techniques thus rely on an underlying reachability analysis and must iterate through time to collect all possible states into a data structure. But the complexity and size of modern integrated circuits, combined with the state space explosion problem, make it impossible to use conventional model checkers on complex designs.
State space reduction techniques are used to combat the state space explosion problem. One technique for state space reduction, the cone of influence reduction, performs formal verification of a given property on the cone of influence rather than on the whole design. The cone of influence is any portion of the circuit design that potentially affects the proof result of the property; the portion of the design outside of the cone of influence does not affect the property. However, the state space explosion problem may still occur with this technique because the cone of influence can be very large in complex designs.
Another technique to address the state space explosion problem uses abstractions in place of certain portions of the cone of influence and verifies a sub-cone of influence, or analysis region. This abstraction allows signals on the boundary of the analysis region can take on any value; thus, abstractions exhibit behavior that is a superset of the actual behavior of the design. If a property is proved true on a portion of a design using an abstraction, it must be true for the entire design because the abstraction contains a superset of the behavior exhibited by the design. But if a property is proved false on a design using an abstraction, the values of the signals on the boundary of the analysis region and abstraction may be causing the false result instead of a real design error. Because the values are a superset of their actual behavior, it is necessary to modify the abstraction.
Accordingly, what are needed are techniques to identify and present inconsistencies between a design and its abstractions during the formal verification process.